Generic{f:T|S(f)}
== R:(T List)
== ((i:, s:(T List). s':T List. (s  s' & R(i,s')))
== & (f:(T). (i:. s:T List. (R(i,s) & (n:{0..||s||}. s[n] = f(n))))  S(f))) 

latex

---

clarification:

generic{i:l}
generic(T; f.S(f))
== R:(T List){i}
== ((i:, s:(T List). s':T List. (s  s'  T List & R(i,s')))
== & (f:(T). (i:. s:T List. (R(i,s) & (n:{0..||s||}. s[n] = f(n)  T)))  S(f))) 

latex

Definitions	, l1  l2, x:AB(x), P  Q, , x:A. B(x), type List, P & Q, x:A. B(x), {i..j}, #$n, ||as||, s = t, l[i], f(a)
FDL editor aliases	generic